Inference at * 1 0 1 
Iof proof for Lemma integer sqrt:



1. n : 
2. n  0 
  r:. (((r * r)  n) & (n < ((r+1) * (r+1)))) 

latex

 by (\p.IntInd (get_int_arg `hn` p) p) 

latex

 1: .....downcase..... NILNIL

 1: 2. n < 0
 1: 3. ((n+1)  0 )  (r:. (((r * r)  (n+1)) & ((n+1) < ((r+1) * (r+1)))))
 1:   (n  0 )  (r:. (((r * r)  n) & (n < ((r+1) * (r+1)))))
 2: .....basecase..... NILNIL

 2: (no hyps)
 2:   (0  0 )  (r:. (((r * r)  0) & (0 < ((r+1) * (r+1)))))
 3: .....upcase..... NILNIL

 3: 2. 0 < n
 3: 3. ((n - 1)  0 )  (r:. (((r * r)  (n - 1)) & ((n - 1) < ((r+1) * (r+1)))))
 3:   (n  0 )  (r:. (((r * r)  n) & (n < ((r+1) * (r+1)))))
 .

Definitions

x:AB(x), P  Q